1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
/*!
An AST for `isotope` expressions.
*/
pub use crate::value::{Dependency, FunctionalLinearity, Linearity, Relationship, Usage, Variance};
use num::BigUint;
use smallvec::SmallVec;
use std::sync::Arc;

mod instant;
mod param;
pub use instant::*;
pub use param::*;

/// An `isotope` expression
#[derive(Debug, Clone, Eq, PartialEq)]
pub enum Expr {
    // === Basic syntax ===
    /// An identifier
    Ident(String),
    /// A hole, "_"
    Hole,
    /// A function application, i.e. S-expression
    Sexpr(Sexpr),
    /// A lambda function
    Lambda(Lambda),

    // === Fundamental typing ===
    /// A pi type
    Pi(Pi),
    /// A typing universe, at a given level
    Universe(u64),

    // === Fundamental lifetimes
    /// A lifetime optionally satisfying a given constraint
    Lifetime(Option<Constraints>),

    // === Primitives ===
    /// The empty type
    Empty,
    /// The unit type
    Unit,
    /// A natural number
    Natural(BigUint),
    /// The type of natural numbers
    Nat,
    /// A boolean value
    Boolean(bool),
    /// The type of booleans
    Bool,

    // === Syntax sugar ===
    /// A scope
    Scope(Scope),
    /// A type of expression. This is a *macro*, using *inference*, and in particular will *not* yield a typeof function!
    TypeOf(Arc<Expr>),
}

impl Expr {
    /// A convenience function to construct to an ident or a hole as an `Option<String>`, the latter represented as `None`
    ///
    /// # Examples
    /// ```rust
    /// # use isotope::ast::*;
    /// assert_eq!(Expr::ident_str("_"), None);
    /// assert_eq!(Expr::ident_str("x"), Some("x".to_owned()));
    /// ```
    pub fn ident_str<S: Into<String> + PartialEq<&'static str>>(ident: S) -> Option<String> {
        if ident.eq(&"_") {
            None
        } else {
            Some(ident.into())
        }
    }
    /// A convenience function to construct an ident, or a hole
    ///
    /// # Examples
    /// ```rust
    /// # use isotope::ast::*;
    /// assert_eq!(Expr::ident("_"), Expr::Hole);
    /// assert_eq!(Expr::ident("x"), Expr::Ident("x".to_owned()));
    /// ```
    pub fn ident<S: Into<String> + PartialEq<&'static str>>(ident: S) -> Expr {
        if let Some(ident) = Expr::ident_str(ident) {
            Expr::Ident(ident)
        } else {
            Expr::Hole
        }
    }
}

impl<'a> From<&'a str> for Expr {
    fn from(s: &'a str) -> Expr {
        Expr::ident(s)
    }
}

impl From<String> for Expr {
    fn from(s: String) -> Expr {
        Expr::ident(s)
    }
}

/// An isotope statement
#[derive(Debug, Clone, Eq, PartialEq)]
pub enum Statement {
    /// An instant having a given set of judgements
    Instant(Instant),
    /// A parameter declaration
    Param(Param),
    /// A let statement
    Let(Let),
}

/// A let statement
#[derive(Debug, Clone, Eq, PartialEq)]
pub struct Let {
    /// The name of the variable being assigned to
    pub name: String,
    /// Optionally, a judgement on the variable being assigned to
    pub judgement: Option<Judgement>,
    /// The value the variable is being assigned
    pub value: Arc<Expr>,
}

/// A typing judgement
#[derive(Debug, Clone, Eq, PartialEq)]
pub struct Judgement {
    /// This judgement's variance
    pub variance: Variance,
    /// Whether this judgement is strict
    pub strict: bool,
    /// The type being judged against
    pub ty: Arc<Expr>,
}

/// The size of a small S-expression
pub const SMALL_SEXPR_SIZE: usize = 2;

/// An S-expression
#[derive(Debug, Clone, Eq, PartialEq)]
pub struct Sexpr(pub SmallVec<[Arc<Expr>; SMALL_SEXPR_SIZE]>);

/// A scope
#[derive(Debug, Clone, Eq, PartialEq)]
pub struct Scope {
    /// The statements in this scope
    pub statements: Vec<Statement>,
    /// The result of this scope
    pub result: Arc<Expr>,
}